{-# OPTIONS_GHC -Wunused-imports #-}
{-# OPTIONS_GHC -Wunused-matches #-}
{-# OPTIONS_GHC -Wunused-binds #-}

{-# LANGUAGE CPP #-}

-- | Attributes: concrete syntax for ArgInfo, esp. modalities.

module Agda.Syntax.Concrete.Attribute where

import Prelude hiding (null)

import Control.Monad (foldM)

#if !MIN_VERSION_base(4,20,0)
import Data.List (foldl')
#endif

import Data.Map (Map)
import qualified Data.Map as Map
import Data.Maybe

import Agda.Syntax.Common
import Agda.Syntax.Concrete (Expr(..), TacticAttribute)
import qualified Agda.Syntax.Concrete as C
import Agda.Syntax.Concrete.Pretty () --instance only
import Agda.Syntax.Common.Pretty (prettyShow)
import Agda.Syntax.Position

import Agda.Utils.Null
import Agda.Utils.Tuple (second)

import Agda.Utils.Impossible

-- | An attribute is a modifier for `ArgInfo`.

data Attribute
  = RelevanceAttribute Relevance
  | QuantityAttribute  Quantity
  | TacticAttribute (Ranged Expr)
  | CohesionAttribute Cohesion
  | PolarityAttribute PolarityModality
  | LockAttribute      Lock
  deriving (Show)

instance HasRange Attribute where
  getRange = \case
    RelevanceAttribute r -> getRange r
    QuantityAttribute q  -> getRange q
    CohesionAttribute c  -> getRange c
    PolarityAttribute p  -> getRange p
    TacticAttribute e    -> getRange e
    LockAttribute _l     -> NoRange

instance SetRange Attribute where
  setRange r = \case
    RelevanceAttribute a -> RelevanceAttribute $ setRange r a
    QuantityAttribute q  -> QuantityAttribute  $ setRange r q
    CohesionAttribute c  -> CohesionAttribute  $ setRange r c
    PolarityAttribute p  -> PolarityAttribute  $ setRange r p
    TacticAttribute e    -> TacticAttribute e  -- -- $ setRange r e -- SetRange Expr not yet implemented
    LockAttribute l      -> LockAttribute l

instance KillRange Attribute where
  killRange = \case
    RelevanceAttribute a -> RelevanceAttribute $ killRange a
    QuantityAttribute q  -> QuantityAttribute  $ killRange q
    CohesionAttribute c  -> CohesionAttribute  $ killRange c
    PolarityAttribute p  -> PolarityAttribute  $ killRange p
    TacticAttribute e    -> TacticAttribute    $ killRange e
    LockAttribute l      -> LockAttribute l

-- | Parsed attribute.

data Attr = Attr
  { attrRange :: Range       -- ^ Range includes the @.
  , attrName  :: String      -- ^ Concrete, user written attribute for error reporting, not including the "@".
  , theAttr   :: Attribute   -- ^ Parsed attribute.
  } deriving (Show)

instance HasRange Attr where
  getRange = attrRange

instance SetRange Attr where
  setRange r (Attr _ x a) = Attr r x a

instance KillRange Attr where
  killRange (Attr _ x a) = Attr noRange x (killRange a)

-- | (Conjunctive constraint.)

type LensAttribute a = (LensRelevance a, LensQuantity a, LensCohesion a, LensModalPolarity a, LensLock a)

-- | Modifiers for 'Relevance'.

relevanceAttributeTable :: [(String, Relevance)]
relevanceAttributeTable =
  [ ("irr"             , Irrelevant      $ OIrrIrr               noRange)
  , ("irrelevant"      , Irrelevant      $ OIrrIrrelevant        noRange)
  , ("shirr"           , ShapeIrrelevant $ OShIrrShIrr           noRange)
  , ("shape-irrelevant", ShapeIrrelevant $ OShIrrShapeIrrelevant noRange)
  , ("relevant"        , Relevant        $ ORelRelevant          noRange)
  ]

-- | Modifiers for 'Quantity'.

quantityAttributeTable :: [(String, Quantity)]
quantityAttributeTable =
  [ ("0"      , Quantity0 $ Q0       noRange)
  , ("erased" , Quantity0 $ Q0Erased noRange)
  -- TODO: linearity
  -- , ("1"      , Quantity1 $ Q1       noRange)
  -- , ("linear" , Quantity1 $ Q1Linear noRange)
  , ("ω"      , Quantityω $ Qω       noRange)
  , ("plenty" , Quantityω $ QωPlenty noRange)
  ]
-- quantityAttributeTable = concat
--   [ map (, Quantity0) [ "0", "erased" ] -- , "static", "compile-time" ]
--   , map (, Quantityω) [ "ω", "plenty" ] -- , "dynamic", "runtime", "unrestricted", "abundant" ]
--   -- , map (, Quantity1)  [ "1", "linear" ]
--   -- , map (, Quantity01) [ "01", "affine" ]
--   ]

cohesionAttributeTable :: [(String, Cohesion)]
cohesionAttributeTable =
  [ ("♭"    , Flat)
  , ("flat" , Flat)
  ]

-- | Information about attributes (attribute, range, printed
-- representation).
--
-- This information is returned by the parser. Code that calls the
-- parser should, if appropriate, complain if support for the given
-- attributes has not been enabled. This can be taken care of by
-- 'Agda.Syntax.Translation.ConcreteToAbstract.checkAttributes', which
-- should not be called until after pragma options have been set.

type Attributes = [Attr]

-- | Modifiers for 'Polarity'.

polarityAttributeTable :: [(String, PolarityModality)]
polarityAttributeTable =
  [ ("unused" , withStandardLock UnusedPolarity)
  , ("++" , withStandardLock StrictlyPositive)
  , ("+" , withStandardLock Positive)
  , ("-" , withStandardLock Negative)
  , ("mixed" , withStandardLock MixedPolarity)]

-- | Modifiers for 'Quantity'.

lockAttributeTable :: [(String, Lock)]
lockAttributeTable = concat
  [ map (, IsNotLock) [ "notlock" ] -- default, shouldn't be used much
  , map (, IsLock LockOTick) [ "tick" ] -- @tick
  , map (, IsLock LockOLock) [ "lock" ] -- @lock
  ]


-- | Concrete syntax for all attributes.

attributesMap :: Map String Attribute
attributesMap = Map.fromListWith __IMPOSSIBLE__ $ concat
  [ map (second RelevanceAttribute) relevanceAttributeTable
  , map (second QuantityAttribute)  quantityAttributeTable
  , map (second CohesionAttribute)  cohesionAttributeTable
  , map (second PolarityAttribute)  polarityAttributeTable
  , map (second LockAttribute)      lockAttributeTable
  ]

-- | Parsing a string into an attribute.

stringToAttribute :: String -> Maybe Attribute
stringToAttribute = (`Map.lookup` attributesMap)

-- | Parsing an expression into an attribute.

exprToAttribute :: Range -> Expr -> Maybe Attribute
exprToAttribute r = \case
  Paren _ (Tactic _ t) -> Just $ TacticAttribute $ Ranged r t
  e -> setRange r $ stringToAttribute $ prettyShow e

-- | Setting an attribute (in e.g. an 'Arg').  Overwrites previous value.

setAttribute :: (LensAttribute a) => Attribute -> a -> a
setAttribute = \case
  RelevanceAttribute r -> setRelevance r
  QuantityAttribute  q -> setQuantity  q
  CohesionAttribute  c -> setCohesion  c
  PolarityAttribute  p -> setModalPolarity p
  LockAttribute      l -> setLock      l
  TacticAttribute _    -> id


-- | Setting some attributes in left-to-right order.
--   Blindly overwrites previous settings.

setAttributes :: (LensAttribute a) => [Attribute] -> a -> a
setAttributes attrs arg = foldl' (flip setAttribute) arg attrs

---------------------------------------------------------------------------
-- * Applying attributes only if they have not been set already.
--   No overwriting.
---------------------------------------------------------------------------

-- | Setting 'Relevance' if unset.

setPristineRelevance :: (LensRelevance a) => Relevance -> a -> Maybe a
setPristineRelevance r a
  | null (getRelevance a) = Just $ setRelevance r a
  | otherwise = Nothing

-- | Setting 'Quantity' if unset.

setPristineQuantity :: (LensQuantity a) => Quantity -> a -> Maybe a
setPristineQuantity q a
  | noUserQuantity a = Just $ setQuantity q a
  | otherwise = Nothing

-- | Setting 'Cohesion' if unset.

setPristineCohesion :: (LensCohesion a) => Cohesion -> a -> Maybe a
setPristineCohesion c a
  | null (getCohesion a) = Just $ setCohesion c a
  | otherwise = Nothing

-- | Setting 'ModalPolarity' if unset.

setPristinePolarity :: (LensModalPolarity a) => PolarityModality -> a -> Maybe a
setPristinePolarity c a
  | getModalPolarity a == defaultPolarity = Just $ setModalPolarity c a
  | otherwise = Nothing

-- | Setting 'Lock' if unset.

setPristineLock :: (LensLock a) => Lock -> a -> Maybe a
setPristineLock q a
  | getLock a == defaultLock = Just $ setLock q a
  | otherwise = Nothing

-- | Setting an unset attribute (to e.g. an 'Arg').

setPristineAttribute :: (LensAttribute a) => Attribute -> a -> Maybe a
setPristineAttribute = \case
  RelevanceAttribute r -> setPristineRelevance r
  QuantityAttribute  q -> setPristineQuantity  q
  CohesionAttribute  c -> setPristineCohesion  c
  PolarityAttribute  p -> setPristinePolarity  p
  LockAttribute      l -> setPristineLock      l
  TacticAttribute{}    -> Just

-- | Setting a list of unset attributes.

setPristineAttributes :: (LensAttribute a) => [Attribute] -> a -> Maybe a
setPristineAttributes attrs arg = foldM (flip setPristineAttribute) arg attrs

---------------------------------------------------------------------------
-- * Filtering attributes
---------------------------------------------------------------------------

isRelevanceAttribute :: Attribute -> Maybe Relevance
isRelevanceAttribute = \case
  RelevanceAttribute q -> Just q
  _ -> Nothing

isQuantityAttribute :: Attribute -> Maybe Quantity
isQuantityAttribute = \case
  QuantityAttribute q -> Just q
  _ -> Nothing

isTacticAttribute :: Attribute -> TacticAttribute
isTacticAttribute = C.TacticAttribute . \case
  TacticAttribute t -> Just t
  _ -> Nothing

relevanceAttributes :: [Attribute] -> [Attribute]
relevanceAttributes = filter $ isJust . isRelevanceAttribute

quantityAttributes :: [Attribute] -> [Attribute]
quantityAttributes = filter $ isJust . isQuantityAttribute

tacticAttributes :: [Attribute] -> [Attribute]
tacticAttributes = filter $ isJust . C.theTacticAttribute . isTacticAttribute
